package var.satisfiability.rules;

import java.util.Iterator;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.RuleLogger;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.ABoxRule;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.syntax.KModality;
import tr.edu.ege.kipler.syntax.TypedModality;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.ModalConcept;


public class BoxConceptRule extends ABoxRule {

	private TypedModality operator;

	private boolean applied;

	@Override
	public boolean isApplied() {
		return applied;
	}

	public BoxConceptRule(TypedModality operator) {
		this.operator = operator;
	}

	public void apply() throws UnsatisfiableException {
		applied = false;
		for (Iterator<Concept> i= getIndividual().conceptIterator(); i.hasNext();) {
			Concept concept = i.next();
			if (concept instanceof ModalConcept) {
				ModalConcept mc = (ModalConcept) concept;
				if (mc.getOperator() instanceof TypedModality
						&& mc.getOperator() instanceof KModality) {
					TypedModality fOperator = (TypedModality) mc.getOperator();
					if (mc.getOperator().isNecessiate()
							&& fOperator.getType().equals(operator.getType())) {
						addNecessiateToAccessibleWorlds(mc, getIndividual());
					}
				}
			}
		}
	}

	protected void addNecessiateToAccessibleWorlds(ModalConcept modalDesc,
			Individual indv) throws UnsatisfiableException {
		ConceptAssertion newCa = new ConceptAssertion(modalDesc.getConcept(),
				indv.getName().toString());
		String relation = ((KModality) modalDesc.getOperator()).getRelation();
		for (World world : getWcs().getAccWorldsByFrom(relation, getWorld())) {
			if (!world.getABox().contains(newCa)) {
				world.add(newCa);
				RuleLogger.getInstance().info(
						"WCS " + getWcs().getId()
								+ " Box Concept Rule: Adding " + newCa
								+ " to the world " + world.getName());
				applied = true;
			}
		}
	}
}
